Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:		a(f,a(f,a(g,a(g,x))))	→ a(g,a(g,a(g,a(f,a(f,a(f,x))))))

There are 6 dependency pairs:


2:		A(f,a(f,a(g,a(g,x))))	→ A(g,a(g,a(g,a(f,a(f,a(f,x))))))
3:		A(f,a(f,a(g,a(g,x))))	→ A(g,a(g,a(f,a(f,a(f,x)))))
4:		A(f,a(f,a(g,a(g,x))))	→ A(g,a(f,a(f,a(f,x))))
5:		A(f,a(f,a(g,a(g,x))))	→ A(f,a(f,a(f,x)))
6:		A(f,a(f,a(g,a(g,x))))	→ A(f,a(f,x))
7:		A(f,a(f,a(g,a(g,x))))	→ A(f,x)

The approximated dependency graph contains one SCC: {5-7}.

Consider the SCC {5-7}. The constraints could not be solved.

Tyrolean Termination Tool (0.18 seconds) --- May 4, 2006